$\forall$$x$, ${\it tg}$:Id, $k$:Knd, $l$:IdLnk, $T$, $A$, $B$:Type, $f$:($A$$\rightarrow$$B$$\rightarrow$($T$ List)).
\\[0ex]((rcv($l$,${\it tg}$) = $k$) $\Rightarrow$ ($T$ = $B$))
\\[0ex]$\Rightarrow$ (($\uparrow$isrcv($k$)) $\Rightarrow$ (destination(lnk($k$)) = source($l$) $\in$ Id))
\\[0ex]$\Rightarrow$ Normal($A$)
\\[0ex]$\Rightarrow$ Normal($B$)
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ $\vdash$${\it es}$.sends1{-}p(${\it es}$;$x$;$A$;$k$;$B$;$l$;${\it tg}$;$T$;$f$)